module Language.Coal.Type (Type, Substitution, resultType, argsType, boolean, integer, function, variables, unify, substitute, compose, isFunction) where

import Language.Coal.Util
import Language.Coal.Error

import Control.Monad

data Type = Variable Integer
	| Application String [Type]
	deriving (Show, Eq, Ord)

integer :: Type
integer = Application "integer" []

boolean :: Type
boolean = Application "boolean" []

function :: [Type] -> Type -> Type
function args result = Application "function" (result : args)

resultType :: Type -> Type
resultType (Application "function" (r:a)) = r

argsType :: Type -> [Type]
argsType (Application "function" (r:a)) = a

isFunction :: Type -> Bool
isFunction (Application "function" _) = True
isFunction _ = False

variables :: [Type]
variables = map Variable [1..]

type Substitution = [(Type, Integer)]

substitute :: Substitution -> Type -> Type
substitute [] t = t
substitute ((st, sn) : rest) t@(Variable n) = if n == sn then st else substitute rest t
substitute l (Application n a) = Application n (map (substitute l) a)


compose :: Substitution -> Substitution  -> Substitution
compose ss s1 = foldl (\ s1 s -> s : mapFst (substitute [s]) s1) s1 ss

unify :: Type -> Type -> CoalError Substitution
unify (Variable v1) (Variable v2) = return $ if v1 == v2 then [] else [(Variable v1, v2)]
unify (Variable v) rt@(Application n t) = if occurs v rt then 
							throwError ("Cannot unify recusive type: " ++ n ++ " " ++ show t ++ " with " ++ show v)
						else
							return [(rt, v)]
unify lt@(Application n t) (Variable v) = if occurs v lt then 
							throwError ("Cannot unify recusive type: " ++ n ++ " " ++ show t ++ " with " ++ show v)
						else
							return [(lt, v)]

unify lt@(Application n1 t1) rt@(Application n2 t2) = if n1 == n2 then do
								ur <- zipWithM unify t1 t2
								return $ foldl compose [] ur	
							else
								throwError ("Cannot unify " ++ n1 ++ " with " ++ n2)

occurs :: Integer -> Type -> Bool
occurs n (Variable vn) = n == vn
occurs n (Application _ a) = any (occurs n) a
